﻿module setOfPairs

type PosPar = (int * int) * (int * int) * Pattern.Pat

type DFR = Dfr of sparseMatrix.matrix * (PosPar list)

(*  the identity DFR *)
let dfrI(n) =
    let idMat = sparseMatrix.I(n)
    Dfr(idMat, sparseMatrix.r(idMat))

let prtR(Dfr(_,r)) =
    let rec prtRList = function
        | ([])                     -> ""
        | ( ((i,j),(i',j'),_)::t ) -> "(" + i.ToString() + "->" + j.ToString() + ", " + (i').ToString() + "->" + (j').ToString() + "), " + prtRList(t);
    prtRList(r)

let prtDfr((Dfr(M,R)) as d) = "\n    M=[ " + sparseMatrix.prt(M) + "]\n    R=[ " + prtR(d) + "]";

(* functions for sorting/merging R's (represented as sorted PosPar lists *)
let lexlt(((a,b),(c,d),_) : PosPar, ((aa,bb),(cc,dd),_)) =
    if (b<bb) then true
    elif (b>bb) then false
    elif (a<aa) then true
    elif (a>aa) then false
    elif (d<dd) then true
    elif (d>dd) then false
    else (c<cc);

let lexEq(((a,b),(c,d),_) : PosPar, ((aa,bb),(cc,dd),_)) =
    if (b<bb) then false
    elif (b>bb) then false
    elif (a<aa) then false
    elif (a>aa) then false
    elif (d<dd) then false
    elif (d>dd) then false
    else (c=cc);

let rec merge = function
    | ([],ys) -> ys
    | (xs,[]) -> xs
    | (x::xs, y::ys) -> if lexlt(x,y) then x::merge(xs,  y::ys)
                        elif lexEq(x,y) then merge(x::xs, ys) else y::merge(x::xs,  ys)

(* sort(already-sorted, yet-not-sorted) *)
let rec sort = function
    | (xs, [])    -> xs
    | (xs, y::ys) -> let rec insert = function
                            | [] -> [y]
                            | (x::xs) -> if lexlt(x,y) then x::insert(xs) elif lexEq(x,y) then x::xs else y::x::xs
                     sort(insert(xs), ys)

let rec filterRDuplicates = function
    | [] -> []
    | [r] -> [r]
    | ((((a,b),(c,d),p) as r1)::(((a',b'),(c',d'),p') as r2)::rs) ->
            if (a=a' && b=b' && c=c' && d=d') then ((a,b),(c,d),Pattern.smaller(p,p'))::filterRDuplicates(rs)
                                                else r1::filterRDuplicates(r2::rs)

(* remove from r those entries which do not correspond to a 1/1+ *)
let filterR(r: PosPar list, m: sparseMatrix.matrix) =
    let ones' = sparseMatrix.ones(m)
    let filtered = List.filter
                            (fun ((a,b),(c,d),_) -> (List.exists (fun (i,j,_,_) -> (i,j)=(a,b)) ones') && (List.exists (fun (i,j,_,_) -> (i,j)=(c,d)) ones') )
                            r
    let order x y = if lexlt(x,y) then 1 else -1
    let sorted = List.sortWith order filtered
    filterRDuplicates(sorted)

(* operations on DFRs *)
let dfrEmpty = function
    | (Dfr(sparseMatrix.M([]),[])) -> true
    | _                   -> false

let dfrsame(Dfr(M1,R1),Dfr(M2,R2)) =
    let rec rSame = function
        | ([],[]) -> true
        | ((a,b,_)::t1,(a',b',_)::t2) -> a=a' && b=b' && rSame(t1,t2)
        | _ -> false

    sparseMatrix.same(M1,M2) && rSame(R1,R2)

(* product of DFR's *)

(* first, product without handling 'diamonds' *)
let rec naiveProd = function
    | ([((a,c),(b,d),p1)],[((e,g),(f,h),p2)]) ->
            let p = Pattern.prod(p1,p2)
            sort ([],
                    (if c=d && d=f then [((a,h),(b,h),p)] else [])  @
                    (if c=d && d=e then [((a,g),(b,g),p)] else [])  @
                    (if c=e && d=f then [((a,g),(b,h),p)] else [])  @
                    (if c=f && d=e then [((a,h),(b,g),p)] else [])  @
                    (if c=e && e=f then [((a,g),(a,h),p)] else [])  @
                    (if d=e && e=f then [((b,g),(b,h),p)] else []) )
    | (R1, R2) ->
            List.fold (fun Ls (p:PosPar) ->
                merge(List.fold (fun Ls (q:PosPar) ->
                                    merge(naiveProd([p],[q]),Ls))
                                    []
                                    R2,
                        Ls))
                        []
                        R1

(* mine R: splits a result of naiveprod into two lists, one containing the positions
    that have to become 2 because of diamonds, the other is the rest of the list,
    to become the R of the product *)
let rec mine = function
    | ([]: PosPar list)           -> ([],[])
    | ((((a,c),(b,d),p) as h)::t) ->
            let (diamonds, rest) = mine(t)
            if (a,c)=(b,d) then ( (a,c,AbstractDomain.polynomial,p)::diamonds, rest )
            else ( diamonds, h::rest )

(* another part of product computation:
    parts of R' created by a 1 in the lhs and a fanout in the rhs. *)
let prod1(lhsM:sparseMatrix.matrix, rhsR:PosPar list) =
    let ones' = sparseMatrix.ones(lhsM)
    List.fold
        (fun acc ((s,j'),(t,j''),p1) ->
                merge (acc,
                        (List.choose (fun (i,j,_,p2) ->
                                        if (s=t) && (s=j)
                                        then Some ((i,j'),(i,j''),Pattern.prod(p2,p1))
                                        else None)
                                        ones')))
        [] rhsR

(* the symmetric thing:
    parts of R' created by a 1 in the rhs and a fanin in the rhs. *)
let prod2(lhsR:PosPar list, rhsM:sparseMatrix.matrix) =
    let ones' = sparseMatrix.ones(rhsM)
    List.fold (fun acc (s,t,_,p1) ->
                    merge (acc,
                            (List.choose (fun ((i,j),(i',j'),p2) ->
                                                if (j=j') && (j=s)
                                                then Some ((i,t),(i',t),Pattern.prod(p2,p1))
                                                else None)
                                            lhsR)))
                [] ones'

let prod(Dfr(A,Ra), Dfr(B,Rb)) =
    let p1 = prod1(A,Rb)
    let p2 = prod2(Ra,B)
    let (d,r) = mine(naiveProd(Ra,Rb));
    let m' = sparseMatrix.sqcup(sparseMatrix.prod(A,B), sparseMatrix.lst2mat(d))
    let m'' = merge(r,p1)
    let m''' = merge(m'',p2)
    let filtered = filterR(m''',m')
    Dfr (m' , filtered)

(* join of DFRs *)

let sqcup(Dfr(M1,R1), Dfr(M2,R2)) =
    let M = sparseMatrix.sqcup(M1,M2)
    Dfr(M, filterR(merge(R1,R2), M))

    (*******NB this is without the iteration count ************)
let loop(l,vars,nonlinear,MR,cmdIdx) =
    (* "loop closure" *)
    let rec fix f x =
        let x' = f x
        if dfrsame(x,x') then x else fix f x'

    let loopAux LC (Dfr(M,R)) =
        let tmpM = LC(M)
        let tmpDFR = Dfr(tmpM, filterR(R,tmpM))
        prod(tmpDFR,tmpDFR)

    fix (loopAux (sparseMatrix.LC (l,nonlinear,cmdIdx))) (sqcup(dfrI(vars,Pattern.Skip),MR))